A:Type, F:(t:({0..t}A)A). CV(F)  A 

latex

Definitions	x:A. B(x), t  T, P  Q, i  j , A  B, A, False, , CV(F), Y, {i..j}, i  j < k, P & Q,
Lemmas	nat wf, int seg wf, nat properties, ge wf, le wf, subtype rel function, subtype rel self